@article{ECMFApaper,
  title={{M}odel {T}ransformations for {M}igrating {L}egacy {M}odels: {A}n {I}ndustrial {C}ase {S}tudy},
  author={Selim, G. and Wang, S. and Cordy, J. and Dingel, J.},
  journal={ECMFA},
  pages={90--101},
  year={2012}
}

@article{giese2010model,
  title={{M}odel {S}ynchronization at {W}ork: {K}eeping {S}ys{ML} and {AUTOSAR} {M}odels {C}onsistent},
  author={Giese, H. and Hildebrandt, S. and Neumann, S.},
  journal={Graph Transformations and Model-Driven Engineering},
  pages={555--579},
  volume={5765},
  year={2010}
}

@InProceedings{daghsen2010applying,
  title={{A}pplying {H}olistic {D}istributed {S}cheduling to {AUTOSAR} {M}ethodology},
  author={Daghsen, A. and Chaaban, K. and Saudrais, S. and Leserf, P.},
  booktitle={ERTSS},
  address={Toulouse, France},
  year={2010}
}

@misc{autosar,
  title={{AUTOSAR} {C}onsortium. {AUTOSAR}, \url{http://{AUTOSAR}.org/}},
  year={2007}
}

@misc{systemp,
  title={{AUTOSAR} {C}onsortium. {AUTOSAR} {S}ystem {T}emplate, \url{http://{AUTOSAR}.org/index.php?p=3\&up=1\&uup=3\& uuup=3\&uuuup=0\& uuuuup=0/{AUTOSAR}\_{TPS}\_{S}ystem{T}emplate.pdf}},
  year={2007}
}

@Article{ANAS,
  title={{A}nalysis of {M}odel {T}ransformations via {A}lloy},
  author={Anastasakis, K. and Bordbar, B. and K{\"u}ster, J.M.},
  journal={MoDeVVa},
  pages={47--56},
  year={2007}
}

@Article{REFC,
  title={{I}terative {D}evelopment of {C}onsistency-{P}reserving {R}ule-{B}ased {R}efactorings},
  author={Becker, B. and Lambers, L. and Dyck, J. and Birth, S. and Giese, H.},
  journal={ICMT},
  pages={123--137},
  year={2011}
}

@Article{VQVT,
  title={{F}ormal {V}erification of {QVT} {T}ransformations for {C}ode {G}eneration},
  author={Stenzel, K. and Moebius, N. and Reif, W.},
  journal={MODELS},
  pages={533--547},
  year={2011}
}

@InProceedings{DEDU,
  title={{T}owards {A}utomated, {F}ormal {V}erification of {M}odel {T}ransformations},
  author={Asztalos, M. and Lengyel, L. and Levendovszky, T.},
  booktitle={ICST},
  pages={15--24},
  address={Paris, France},
  year={2010},
}

@Article{MLVW,
  title={{M}etamodel-{B}ased {M}odel {C}onformance and {M}ultiview {C}onsistency {C}hecking},
  author={Paige, R.F. and Brooke, P.J. and Ostroff, J.S.},
  journal={TOSEM},
  volume={16},
  number={3},
  pages={1-48},
  year={2007},
}

@Article{LEVI,
  title={{A} {T}echnique for {A}utomatic {V}alidation of {M}odel {T}ransformations},
  author={L{\'u}cio, L. and Barroca, B. and Amaral, V.},
  journal={MODELS},
  pages={136--150},
  year={2010}
}

@Article{CRSP,
  title={{V}erifying {M}odel {T}ransformations by {S}tructural {C}orrespondence},
  author={Narayanan, A. and Karsai, G.},
  journal={EASST},
  volume={10},
  number={0},
  year={2008}
}

 @InProceedings{a15,
  title={{T}he {M}otorola {WEAVR}: {M}odel {W}eaving in a {L}arge {I}ndustrial {C}ontext},
  author={Cottenier, T. and Van Den Berg, A. and Elrad, T.},
  booktitle={AOSD},
  volume={32},
  address={Vancouver, Canada},
  year={2007}
}

@InProceedings{indusREV,
  title={{W}here is the {P}roof?-{A} {R}eview of {E}xperiences from {A}pplying {MDE} in {I}ndustry},
  author={Mohagheghi, P. and Dehlen, V.},
  booktitle={ECMDA--FA},
  pages={432--443},
  year={2008}
}

@InProceedings{Buettner2012MoDELS,
  author = {Fabian B{\"u}ttner and Marina Egea and Jordi Cabot},
  title = {{O}n {V}erifying {ATL} {T}ransformations {U}sing {O}ff-the-{S}helf {SMT} {S}olvers},
  booktitle = {MODELS},
  year = {2012},
  volume = {7590},
  series = {LNCS},
  pages = {432-448},
  abstract = {MDE is a software development process where models constitute pivotal
	elements of the software to be built. If models are well-specified,
	transformations can be employed for various purposes, e.g., to produce
	final code. However, transformations are only meaningful when they
	are 'correct': they must produce valid models from valid input models.
	A valid model has conformance to its meta-model and fulfils its constraints,
	usually written in OCL. In this paper, we propose a novel methodology
	to perform automatic, unbounded verification of ATL transformations.
	Its main component is a novel first-order semantics for ATL transformations,
	based on the interpretation of the corresponding rules and their
	execution semantics as first-order predicates. Although, our semantics
	is not complete, it does cover a significant subset of the ATL language.
	Using this semantics, transformation correctness can be automatically
	verified with respect to non-trivial OCL pre- and postconditions
	by using SMT solvers, e.g. Z3 and Yices.}
}


@InProceedings{Buettner2012ICFEM,
  author = {Fabian B{\"u}ttner and Marina Egea and Jordi Cabot and Martin Gogolla},
  title = {{V}erification of {ATL} {T}ransformations {U}sing {T}ransformation
	{M}odels and {M}odel {F}inders},
  booktitle = {ICFEM},
  year = {2012},
  volume = {7635},
  series = {LNCS},
  pages = {198-213}
}

@InProceedings{Kuhlmann2011,
  author = {Mirco Kuhlmann and Lars Hamann and Martin Gogolla},
  title = {{E}xtensive {V}alidation of {OCL} {M}odels by {I}ntegrating {SAT}
	{S}olving into {USE}},
  booktitle = {TOOLS},
  year = {2011},
  volume = {6705},
  series = {LNCS},
  pages = {290-306},
  file = {Kuhlmann2011.pdf:Kuhlmann2011.pdf:PDF},
  keywords = {model finder;}
}

@InProceedings{Tisi2009HOT,
  author = {Massimo Tisi and Fr{\'e}d{\'e}ric Jouault and Piero Fraternali and Stefano
	Ceri and Jean B{\'e}zivin},
  title = {{O}n the {U}se of {H}igher-{O}rder {M}odel {T}ransformations},
  booktitle = {ECMDA-FA},
  year = {2009},
  volume = {5562},
  series = {LNCS}
}

@INPROCEEDINGS{Sen2009b,
  author = {Sagar Sen and Naouel Moha and Benoit Baudry and Jean-Marc J{\'e}z{\'e}quel},
  title = {{M}eta-model {P}runing},
  booktitle = {MODELS},
  year = {2009},
  volume = {5795},
  series = {LNCS},
  pages = {32-46}
}


@inproceedings{Jacobs01,
  author    = {Bart Jacobs and
               Erik Poll},
  title     = {{A} {L}ogic for the {J}ava {M}odeling {L}anguage {JML}},
  year      = {2001},
  pages     = {284-299},
  booktitle     = {FASE},
  series    = {LNCS},
  volume    = {2029},
}

@Misc{ATLZoo,
  key = 	 {ZOO},
  title = 	 {{T}he {Z}oo of {ATL} {T}ransformations},
  note = 	 {available online, \url{http://www.eclipse.org/atl/atlTransformations/}}
}

@Misc{USE,
  key = 	 {USE},
  title = 	 {{T}he {USE V}alidator},
  note = 	 {available online, \url{http://sourceforge.net/projects/useocl/files/ Plugins/ModelValidator/}}
}

@Misc{ZOO,
  key = 	 {ZOO},
  title = 	 {{T}he {ATL T}ransformation {Z}oo},
  note = 	 {available online, \url{http://www.eclipse.org/atl/atlTransformations/}}
}

@InProceedings{Torlak2007Kodkod,
  author = {Emina Torlak and Daniel Jackson},
  title = {{K}odkod: {A} {R}elational {M}odel {F}inder},
  booktitle = {TACAS},
  year = {2007},
  volume = {4424},
  series = {LNCS}
}

@InProceedings{CHALL,
	Address = {Bilbao, Spain},
	Author = {Baudry, B. and Dinh-Trong, T. and Mottu, J.M. and Simmonds, D. and France, R. and Ghosh, S. and Fleurey, F. and Le Traon, Y.},
	Booktitle = {Integration of Model Driven Development and Model Driven Testing},
	Title = {{M}odel {T}ransformation {T}esting {C}hallenges}, 
	Year = {2006}
}

@InProceedings{COMP,
  title={{R}eusable {MDA} {C}omponents: {A} {T}esting-for-{T}rust {A}pproach},
  author={Mottu, J.M. and Baudry, B. and Le Traon, Y.},
  booktitle={MODELS},
  pages={589--603},
  address={Genova, Italy},
  year={2006}
}

@InProceedings{GOGO,
  title={{T}ractable {M}odel {T}ransformation {T}esting},
  author={Gogolla, M. and Vallecillo, A.},
  booktitle={ECMFA},
  pages={221--236},
  address={Birmingham, UK},
  year={2011}
}

@ARTICLE{Troya2011ATL,
  author = {Javier Troya and Antonio Vallecillo},
  title = {{A} {R}ewriting {L}ogic {S}emantics for {ATL}},
  journal = {Journal of Object Technology},
  year = {2011},
  volume = {10},
  pages = {5: 1-29},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.5381/jot.2011.10.1.a5},
  file = {Troya2011ATL.pdf:Troya2011ATL.pdf:PDF}
}


@article{Guerra2013,
  author    = {Esther Guerra and
               Juan de Lara and
               Manuel Wimmer and
               Gerti Kappel and
               Angelika Kusel and
               Werner Retschitzegger and
               Johannes Sch{\"o}nb{\"o}ck and
               Wieland Schwinger},
  title     = {{A}utomated {V}erification of {M}odel {T}ransformations {B}ased on
               {V}isual {C}ontracts},
  journal   = {Automated Software Engineering},
  volume    = {20},
  number    = {1},
  year      = {2013},
  pages     = {5-46},
  ee        = {http://dx.doi.org/10.1007/s10515-012-0102-y},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@INPROCEEDINGS{Inaba2011,
  author = {Kazuhiro Inaba and Soichiro Hidaka and Zhenjiang Hu and Hiroyuki
	Kato and Keisuke Nakano},
  title = {{G}raph-{T}ransformation {V}erification {U}sing {M}onadic {S}econd-{O}rder {L}ogic},
  booktitle = {PPDP},
  year = {2011},
  pages = {17-28}
}


@INPROCEEDINGS{Rensink2008,
  author = {Arend Rensink},
  title = {{E}xplicit {S}tate {M}odel {C}hecking for {G}raph {G}rammars},
  booktitle = {Concurrency, Graphs and Models},
  year = {2008},
  volume = {5065},
  series = {LNCS},
  pages = {114-132}
}


@INPROCEEDINGS{Baresi2006,
  author = {Luciano Baresi and Paola Spoletini},
  title = {{O}n the {U}se of {A}lloy to {A}nalyze {G}raph {T}ransformation {S}ystems},
  booktitle = {ICGT},
  year = {2006},
  volume = {4178},
  series = {LNCS},
  pages = {306-320},
  owner = {fabian},
  timestamp = {2012.04.20}
}

@ARTICLE{Cabot2010,
  author = {Jordi Cabot and Robert Claris{\'o} and Esther Guerra and Juan de
	Lara},
  title = {{V}erification and {V}alidation of {D}eclarative {M}odel-to-{M}odel {T}ransformations
	{T}hrough {I}nvariants},
  journal = {Systems and Software},
  year = {2010},
  volume = {83},
  pages = {283--302},
  number = {2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@ARTICLE{Jouault2008ATL,
  author = {Fr{\'e}d{\'e}ric Jouault and Freddy Allilaire and Jean B{\'e}zivin and Ivan Kurtev},
  title = {{ATL}: {A} {M}odel {T}ransformation {T}ool},
  journal = {Sci. Comput. Program.},
  year = {2008},
  volume = {72},
  pages = {31--39},
  number = {1-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@ARTICLE{Cariou2009,
  author = {Eric Cariou and Nicolas Belloir and Franck Barbier and Nidal Djemam},
  title = {{OCL} {C}ontracts for the {V}erification of {M}odel {T}ransformations},
  journal = {EASST},
  year = {2009},
  volume = {24},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://journal.ub.tu-berlin.de/index.php/eceasst/article/view/326},
  owner = {fabian},
  timestamp = {2012.04.20}
}

@INPROCEEDINGS{Braga2011,
  author = {Christiano Braga and Roberto Menezes and Thiago Comicio and Cassio
	Santos and Edson Landim},
  title = {{O}n the {S}pecification, {V}erification and {I}mplementation of
	{M}odel {T}ransformations with {T}ransformation {C}ontracts},
  booktitle = {SBMF},
  year = {2011},
  volume = {7021},
  series = {LNCS},
  pages = {108-123}
}

@ARTICLE{Jackson2013,
  author = {Ethan Jackson and Tihamer Levendovszky and Daniel Balasubramanian},
  title = {{A}utomatically reasoning about metamodeling},
  journal = {SoSyM},
  year = {2013},
  pages = {1-15},
  doi = {10.1007/s10270-013-0315-y},
  file = {Jackson2013.pdf:Jackson2013.pdf:PDF},
  issn = {1619-1366},
  keywords = {Metamodeling; Formal specifications; Automated analysis},
  url = {http://dx.doi.org/10.1007/s10270-013-0315-y}
}

@INPROCEEDINGS{Cabot2007,
  author = {Jordi Cabot and Robert Claris{\'o} and Daniel Riera},
  title = {{UML}to{CSP}: {A} {T}ool for the {F}ormal {V}erification of {UML}/{OCL} {M}odels
	{U}sing {C}onstraint {P}rogramming},
  booktitle = {ASE},
  year = {2007},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://doi.acm.org/10.1145/1321631.1321737},
  isbn = {978-1-59593-882-4 },
  keywords = {model finder;},
  owner = {fabian},
  timestamp = {2012.04.20}
}

@ARTICLE{Queralt2012,
  author = {Anna Queralt and Ernest Teniente},
  title = {{V}erification and {V}alidation of {UML} {C}onceptual {S}chemas with
	{OCL} {C}onstraints},
  journal = {TOSEM},
  year = {2012},
  volume = {21},
  pages = {13},
  number = {2},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://doi.acm.org/10.1145/2089116.2089123},
  file = {Queralt2012.pdf:Queralt2012.pdf:PDF}
}

@INPROCEEDINGS{Gonzalez2012,
  author = {Gonz{\'a}lez P{\'e}rez, Carlos Alberto and B{\"u}ttner, Fabian and Claris{\'o},
	Robert and Cabot, Jordi},
  title = {{EMF}to{CSP}: {A} {T}ool for the {L}ightweight {V}erification of
	{EMF} {M}odels},
  booktitle = {FormSERA},
  pages={44--50 },
  year = {2012},
  address = {Zurich, Switzerland},
  url = {http://hal.inria.fr/hal-00688039}
}

@article{Brucker2009,
  author    = {Achim D. Brucker and
               Burkhart Wolff},
  title     = {{S}emantics, {C}alculi, and {A}nalysis for {O}bject-{O}riented {S}pecifications},
  journal   = {Acta Informatica},
  volume    = {46},
  number    = {4},
  year      = {2009},
  pages     = {255--284},
  ee        = {http://dx.doi.org/10.1007/s00236-009-0093-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
